$\forall$$M$:MsgA, $x$:Id, $s_{1}$, $s_{2}$:$M$.(timed)state. ma{-}x{-}tequiv($M$;$x$;$s_{1}$;$s_{2}$) $\in$ $\mathbb{P}$